R-frame-compat(A;B)
== if Reffect?(A)
== if if Rframe?(B) Rframe-x(B) = Reffect-x(A)  (Reffect-knd(A)  Rframe-L(B))
== if i; Raframe?(B) Raframe-k(B) = Reffect-knd(A)  (Reffect-x(A)  Raframe-L(B))
== if i; Rrframe?(B) Rrframe-x(B)  dom(Reffect-ds(A))  (Reffect-knd(A)  Rrframe-L(B))
== if else True fi
== i; Rsends?(A)
== i; if Rsframe?(B)
== i; if Rsframe-lnk(B) = Rsends-l(A)
== i; if  (Rsframe-tag(B)  map(p.1of(p);Rsends-g(A)))
== i; if  (Rsends-knd(A)  Rsframe-L(B))
== i; i; Rbframe?(B) Rbframe-k(B) = Rsends-knd(A)  (Rsends-l(A)  Rbframe-L(B))
== i; i; Rrframe?(B) Rrframe-x(B)  dom(Rsends-ds(A))  (Rsends-knd(A)  Rrframe-L(B))
== i; else True fi
== i; Rpre?(A)
== i; if Rrframe?(B) Rrframe-x(B)  dom(Rpre-ds(A))  (locl(Rpre-a(A))  Rrframe-L(B))
== i; else True fi
== else True fi 

latex

---

clarification:

R-frame-compat(A;B)
== if Reffect?(A)
== if if Rframe?(B) Rframe-x(B) = Reffect-x(A)  Id  (Reffect-knd(A)  Rframe-L(B)  Knd)
== if i; Raframe?(B) Raframe-k(B) = Reffect-knd(A)  Knd  (Reffect-x(A)  Raframe-L(B)  Id)
== if i; Rrframe?(B)
== if i; fpf-dom(IdDeq; Rrframe-x(B); Reffect-ds(A))  (Reffect-knd(A)  Rrframe-L(B)  Knd)
== if else True fi
== i; Rsends?(A)
== i; if Rsframe?(B)
== i; if Rsframe-lnk(B) = Rsends-l(A)  IdLnk
== i; if  (Rsframe-tag(B)  map(p.1of(p);Rsends-g(A))  Id)
== i; if  (Rsends-knd(A)  Rsframe-L(B)  Knd)
== i; i; Rbframe?(B) Rbframe-k(B) = Rsends-knd(A)  Knd  (Rsends-l(A)  Rbframe-L(B)  IdLnk)
== i; i; Rrframe?(B)
== i; i; fpf-dom(IdDeq; Rrframe-x(B); Rsends-ds(A))  (Rsends-knd(A)  Rrframe-L(B)  Knd)
== i; else True fi
== i; Rpre?(A)
== i; if Rrframe?(B)
== i; if fpf-dom(IdDeq; Rrframe-x(B); Rpre-ds(A))  (locl(Rpre-a(A))  Rrframe-L(B)  Knd)
== i; else True fi
== else True fi 

latex

Definitions

Reffect?(x1), Rframe?(x1), Rframe-x(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Reffect-x(x1), Raframe-L(x1), Reffect-ds(x1), Reffect-knd(x1), Rsends?(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsframe-tag(x1), map(f;as), x.A(x), 1of(t), Rsends-g(x1), Id, Rsframe-L(x1), Rbframe?(x1), s = t, Rbframe-k(x1), Rsends-l(x1), Rbframe-L(x1), IdLnk, Rsends-ds(x1), Rsends-knd(x1), Rpre?(x1), if b t else f fi, Rrframe?(x1), P  Q, b, x  dom(f), IdDeq, Rrframe-x(x1), Rpre-ds(x1), (x  l), locl(a), Rpre-a(x1), Rrframe-L(x1), Knd, True

FDL editor aliases

R-frame-compat